Termination w.r.t. Q proof of /tmp/tmp-0KGHs/ExIntrod_GM04

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

a__nats → a__adx(a__zeros)
a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
a__tl(cons(X, Y)) → mark(Y)
mark(nats) → a__nats
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(tl(X)) → a__tl(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__nats → nats
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)
a__tl(X) → tl(X)

Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__nats → a__adx(a__zeros)
a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
a__tl(cons(X, Y)) → mark(Y)
mark(nats) → a__nats
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(tl(X)) → a__tl(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__nats → nats
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)
a__tl(X) → tl(X)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

a__nats → a__adx(a__zeros)
a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
a__tl(cons(X, Y)) → mark(Y)
mark(nats) → a__nats
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(tl(X)) → a__tl(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__nats → nats
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)
a__tl(X) → tl(X)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

a__tl(cons(X, Y)) → mark(Y)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(a__adx(x₁)) = 2·x₁
POL(a__hd(x₁)) = x₁
POL(a__incr(x₁)) = x₁
POL(a__nats) = 0
POL(a__tl(x₁)) = 2 + 2·x₁
POL(a__zeros) = 0
POL(adx(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(hd(x₁)) = x₁
POL(incr(x₁)) = x₁
POL(mark(x₁)) = x₁
POL(nats) = 0
POL(s(x₁)) = x₁
POL(tl(x₁)) = 2 + 2·x₁
POL(zeros) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__nats → a__adx(a__zeros)
a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
mark(nats) → a__nats
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(tl(X)) → a__tl(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__nats → nats
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)
a__tl(X) → tl(X)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

a__nats → a__adx(a__zeros)
a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
mark(nats) → a__nats
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(tl(X)) → a__tl(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__nats → nats
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)
a__tl(X) → tl(X)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

a__nats → a__adx(a__zeros)
mark(nats) → a__nats
mark(tl(X)) → a__tl(mark(X))

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(a__adx(x₁)) = 2·x₁
POL(a__hd(x₁)) = x₁
POL(a__incr(x₁)) = x₁
POL(a__nats) = 2
POL(a__tl(x₁)) = 2 + x₁
POL(a__zeros) = 0
POL(adx(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + 2·x₂
POL(hd(x₁)) = x₁
POL(incr(x₁)) = x₁
POL(mark(x₁)) = 2·x₁
POL(nats) = 2
POL(s(x₁)) = x₁
POL(tl(x₁)) = 2 + x₁
POL(zeros) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__nats → nats
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)
a__tl(X) → tl(X)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__nats → nats
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)
a__tl(X) → tl(X)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

a__nats → nats
a__tl(X) → tl(X)

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(a__adx(x₁)) = x₁
POL(a__hd(x₁)) = 2·x₁
POL(a__incr(x₁)) = x₁
POL(a__nats) = 2
POL(a__tl(x₁)) = 2 + 2·x₁
POL(a__zeros) = 0
POL(adx(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁ + 2·x₂
POL(hd(x₁)) = 2·x₁
POL(incr(x₁)) = x₁
POL(mark(x₁)) = 2·x₁
POL(nats) = 1
POL(s(x₁)) = x₁
POL(tl(x₁)) = 1 + x₁
POL(zeros) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

a__zeros → cons(0, zeros)
a__hd(cons(X, Y)) → mark(X)
mark(hd(X)) → a__hd(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__zeros → zeros

Used ordering:
Polynomial interpretation [25]:

POL(0) = 0
POL(a__adx(x₁)) = 1 + 2·x₁
POL(a__hd(x₁)) = 2 + 2·x₁
POL(a__incr(x₁)) = x₁
POL(a__zeros) = 1
POL(adx(x₁)) = 1 + 2·x₁
POL(cons(x₁, x₂)) = x₁ + x₂
POL(hd(x₁)) = 2 + 2·x₁
POL(incr(x₁)) = x₁
POL(mark(x₁)) = 1 + 2·x₁
POL(s(x₁)) = x₁
POL(zeros) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
a__adx(X) → adx(X)
a__incr(X) → incr(X)
a__hd(X) → hd(X)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
a__adx(X) → adx(X)
a__incr(X) → incr(X)
a__hd(X) → hd(X)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

mark(adx(X)) → a__adx(mark(X))

Used ordering:
Polynomial interpretation [25]:

POL(a__adx(x₁)) = 1 + 2·x₁
POL(a__hd(x₁)) = 2 + x₁
POL(a__incr(x₁)) = x₁
POL(a__zeros) = 0
POL(adx(x₁)) = 1 + 2·x₁
POL(cons(x₁, x₂)) = 2·x₁ + x₂
POL(hd(x₁)) = 2 + x₁
POL(incr(x₁)) = x₁
POL(mark(x₁)) = 2·x₁
POL(s(x₁)) = x₁
POL(zeros) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
a__adx(X) → adx(X)
a__incr(X) → incr(X)
a__hd(X) → hd(X)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
a__adx(X) → adx(X)
a__incr(X) → incr(X)
a__hd(X) → hd(X)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

mark(zeros) → a__zeros
a__adx(X) → adx(X)
a__incr(X) → incr(X)
a__hd(X) → hd(X)

Used ordering:
Polynomial interpretation [25]:

POL(a__adx(x₁)) = 2 + 2·x₁
POL(a__hd(x₁)) = 2 + 2·x₁
POL(a__incr(x₁)) = 2 + 2·x₁
POL(a__zeros) = 1
POL(adx(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁ + x₂
POL(hd(x₁)) = 1 + x₁
POL(incr(x₁)) = 1 + 2·x₁
POL(mark(x₁)) = 2·x₁
POL(s(x₁)) = 1 + x₁
POL(zeros) = 1

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
mark(incr(X)) → a__incr(mark(X))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
mark(incr(X)) → a__incr(mark(X))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))

Used ordering:
Polynomial interpretation [25]:

POL(a__adx(x₁)) = 1 + 2·x₁
POL(a__incr(x₁)) = x₁
POL(adx(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁ + 2·x₂
POL(incr(x₁)) = x₁
POL(mark(x₁)) = x₁
POL(s(x₁)) = x₁

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__incr(cons(X, Y)) → cons(s(X), incr(Y))
mark(incr(X)) → a__incr(mark(X))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

a__incr(cons(X, Y)) → cons(s(X), incr(Y))
mark(incr(X)) → a__incr(mark(X))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

a__incr(cons(X, Y)) → cons(s(X), incr(Y))
mark(incr(X)) → a__incr(mark(X))

Used ordering:
Polynomial interpretation [25]:

POL(a__incr(x₁)) = 1 + 2·x₁
POL(cons(x₁, x₂)) = 2 + 2·x₁ + x₂
POL(incr(x₁)) = 2 + 2·x₁
POL(mark(x₁)) = 2·x₁
POL(s(x₁)) = x₁

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RRRPoloQTRSProof

                        ↳ QTRS

                          ↳ RRRPoloQTRSProof

                            ↳ QTRS

                              ↳ RRRPoloQTRSProof

                                ↳ QTRS

                                  ↳ RisEmptyProof

Q restricted rewrite system:
R is empty.
Q is empty.

The TRS R is empty. Hence, termination is trivially proven.